\begin{tabbing}
$\forall$${\it es}$:ES, $e$, ${\it e'}$:E.
\\[0ex]($\uparrow$isrcv($e$))
\\[0ex]$\Rightarrow$ ($\uparrow$isrcv(${\it e'}$))
\\[0ex]$\Rightarrow$ \=(($e$ = ${\it e'}$)\+
\\[0ex]$\Leftarrow\!\Rightarrow$ (sender($e$) = sender(${\it e'}$) $\in$ E \& lnk($e$) = lnk(${\it e'}$) $\in$ IdLnk \& index($e$) = index(${\it e'}$) $\in$ $\mathbb{Z}$))
\-
\end{tabbing}